Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    p(0)  → 0
2:    p(s(X))  → X
3:    leq(0,Y)  → true
4:    leq(s(X),0)  → false
5:    leq(s(X),s(Y))  → leq(X,Y)
6:    if(true,X,Y)  → X
7:    if(false,X,Y)  → Y
8:    diff(X,Y)  → if(leq(X,Y),0,s(diff(p(X),Y)))
There are 5 dependency pairs:
9:    LEQ(s(X),s(Y))  → LEQ(X,Y)
10:    DIFF(X,Y)  → IF(leq(X,Y),0,s(diff(p(X),Y)))
11:    DIFF(X,Y)  → LEQ(X,Y)
12:    DIFF(X,Y)  → DIFF(p(X),Y)
13:    DIFF(X,Y)  → P(X)
The approximated dependency graph contains 2 SCCs: {9} and {12}.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006